p,q:(n:  base-domain-type(n)). eq_bd(p; q)   

latex

Definitions

x. t(x), True, T, P  Q, guard(T), sq_type(T), ff, P  Q, P  Q, prop{i:l}, P  Q, P  Q, tt, t.2, if b then t else f fi , t.1, band(p; q), eq_bd(p; q), t  T, x:A. B(x), x(s), Unit, bor(p; q), (i = j), , base-domain-type(n),

Lemmas

base-domain-type wf, bfalse wf, btrue wf, Knd wf, eq knd wf, pi2 wf, Id wf, IdLnk wf, pi1 wf, eq lnk wf, not functionality wrt iff, assert of bnot, and functionality wrt iff, assert of band, bnot thru bor, true wf, squash wf, eqff to assert, not wf, bnot wf, band wf, eq id wf, or functionality wrt iff, assert of bor, bor wf, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool wf, eq int wf